the_w:World, e, e':E. e = e'  e = e' 

latex

Definitions	p  q, a = b, i=j, , Id, P  Q, P & Q, P  Q, Prop, E, World, P  Q, b, p = q, x:A. B(x), t  T
Lemmas	w-eq-E wf, assert wf, assert-w-eq-E, world wf, w-E wf, Id wf, eq int wf, eq id wf, band wf, assert of eq int, assert-eq-id, and functionality wrt iff, assert of band, iff transitivity